package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.ClockGuard;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.SimpleClockGuard;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class Toy5 {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Toy5");
		 
         // Variables
         TypedData v1 = new TypedData("v1", Constants.TYPE_INTEGER);
         tiosts.addVariable(v1);
         TypedData v2 = new TypedData("v2", Constants.TYPE_INTEGER);
         tiosts.addVariable(v2);
         
         //Clocks
         
         tiosts.addClock("clock"); 		
         SimpleClockGuard guard1 = new SimpleClockGuard(1, "clock", Constants.GUARD_GT, "1");
 		 ClockGuard clockGuard = new ClockGuard();
 		 clockGuard.addSimpleClockGuard(guard1);
         
         // There are no parameters       
         
         // Input, output, and internal actions
         Action init1 = new Action("Init1", Constants.ACTION_INTERNAL);
         tiosts.addAction(init1);
         Action a = new Action("a", Constants.ACTION_INPUT);
         tiosts.addAction(a);
         tiosts.addActionParameter(v1);
         Action b = new Action("b", Constants.ACTION_INPUT);
         tiosts.addAction(b);
         tiosts.addActionParameter(v2);
         
         // Locations
         Location start = new Location("Start1");
         tiosts.addLocation(start);
         Location s1 = new Location("S1");
         tiosts.addLocation(s1);
         Location s2 = new Location("S2");
         tiosts.addLocation(s2);        
         Location s3 = new Location("S3");
         tiosts.addLocation(s3);
         
         // Initial Condition
         tiosts.setInitialCondition("v1 > 0");
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("Start1", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init1, null, null, "S1");
         tiosts.createTransition("S1", Constants.GUARD_TRUE, clockGuard, a, "v1 := 0", null, Constants.DEADLINE_EAGER, "S2");
         tiosts.createTransition("S1", Constants.GUARD_TRUE, clockGuard, b, "v2 := 0", null, Constants.DEADLINE_DELAYABLE, "S3");
         
         return tiosts;
		 
	 }

}
